МІНІСТЕРСТВО ОСВІТИ І НАУКИ УКРАЇНИ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ «ЛЬВІСЬКА ПОЛІТЕХНІКА» Кафедра ІСМ Звіт До лабораторної роботи №6 З дисципліни: «Методи та системи штучного інтелекту» На тему: «Алгоритм методу резолюцій доведення теорем у штучному інтелекті»  Львів-2017 Мета роботи: полягає у вивченні алгоритму методу резолюції доведення теорем у штучному інтелекті та алгоритму уніфікації. Теоретичні відомості / Завдання лабораторної роботи: Скласти програму, яка дозволяє доводити теореми у штучному інтелекті застосуванням алгоритму резолюції. Програма повинна доводити невиконання заданої множини диз’юнктів або демонструвати її виконання. Алгоритм резолюції повинен виконуватись для множини диз’юнктів у логіці висловлень. Результати виконання роботи:  package vovk_2; /** * * @author asuspk */ public class tata extends javax.swing.JFrame { /** * Creates new form tata */ public tata() { initComponents(); } private void jButton1ActionPerformed(java.awt.event.ActionEvent evt) { jTextArea1.setText("Якщо " + jTextField1.getText() + " " + jTextField3.getText() + " а " + jTextField2.getText() + " " + jTextField1.getText() + " то " + jTextField2.getText() + " " + jTextField3.getText()); private void jButton2ActionPerformed(java.awt.event.ActionEvent evt) { jTextArea2.setText("Якщо " + jTextField4.getText() + " то я " + jTextField5.getText() + " .Інакше я " + jTextField6.getText()); // TODO add your handling code here: } public static void main(String args[]) { java.awt.EventQueue.invokeLater(new Runnable() { public void run() { new tata().setVisible(true); } }); } private javax.swing.JButton jButton1; private javax.swing.JButton jButton2; private javax.swing.JLabel jLabel1; private javax.swing.JLabel jLabel2; private javax.swing.JLabel jLabel3; private javax.swing.JLabel jLabel4; private javax.swing.JLabel jLabel5; private javax.swing.JLabel jLabel6; private javax.swing.JLabel jLabel7; private javax.swing.JLabel jLabel8; private javax.swing.JScrollPane jScrollPane1; private javax.swing.JScrollPane jScrollPane2; private javax.swing.JSeparator jSeparator1; private javax.swing.JTextArea jTextArea1; private javax.swing.JTextArea jTextArea2; private javax.swing.JTextField jTextField1; private javax.swing.JTextField jTextField2; private javax.swing.JTextField jTextField3; private javax.swing.JTextField jTextField4; private javax.swing.JTextField jTextField5; private javax.swing.JTextField jTextField6; // End of variables declaration }  В даній програмі використовувався тестовий інтерфейс. Програма генерує резолюцію та логіку Арістотеля. / Рис. 1. Результат виконання програми Висновок Виконавши дану лабораторну роботу, вивчила алгоритм методу резолюції доведення теорем у штучному інтелекті та алгоритм уніфікації та їх використання.